Corelab Seminar
2016-2017
Antonis Achilleos
The complexity of identifying characteristic formulas for μHML
Abstract.
We examine the complexity of determining whether a formula οf the maximal-fixed-point fragment of the Henessy Milner logic with recursion characterizes a process up to bisimulation equivalence. We discover that the problem is EXP-complete. The decision procedure that establishes this upper bound is based on a two-player game.